COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	Biography:
C00011 ENDMK
C⊗;
Biography:

John Richardson Allen
 Born: September 2, 1937; married with two children

Education:
 1959 B.A. in mathematics (with honors) 
 Michigan Technological University
 Houghton, Michigan

 1962 M.A. in mathematics
 University of California
 Santa Barbara, Cal

 1966-1969 graduate work in Computer Science
 Stanford University
 Stanford, Cal

Experience:
 1959-1960 mathematical programmer
 Burroughs Corp.
 Sierra Madre, Cal
  (machine language programming of various mathematical problems.)

 1963-1965 mathematical and systems programmer
 General Motors Research Labs
 Goleta, Cal
  (general mathematical programming; developed LISP for IBM7040;
   modification of operating system for 7040)

 1965-1966 systems programmer
 Stanford A.I. Project
 Stanford, Cal
  (designed and developed time-sharing system for PDP-1; implemented
   Culler-Fried system for this system; maintained early PDP-6 monitors)

 1966-1968 student research associate
 Stanford A.I. Laboratory
 Stanford, Cal
  (modified MAC-LISP to Stanford-LISP; maintained LISP complier and system;
   developed simple LISP editor and interfaced LISP to machine language
   programs; designed LISP's big-number programs. Research in resolution
   theory and interactive theorem-proving)


 1969 systems programmer and researcher
 Institute for Mathematical Studies in Social Sciences
 Stanford University
 Stanford, Cal
   (continuing research in theorem-proving; general consultant on  PDP-10
    system, and applications of theorem-proving to educational areas)

 1970-1972 Assistant Professor of Computer Science
 Computer Science Dept
 University of California
 Los Angeles, Cal
   (taught courses in basic machine and systems orgainzation, data  structures,
    compiler construction, and semantics of programming languages. Organized
    seminar on extensible languages, correctness and language design. Research
    in theorem-proving and language design)

 1972 to present Research Associate
 Stanford A.I. Lab
 Computer Science Dept.
 Stanford Cal
    (Theory and applications of theorem-proving, automatic programming,
     and verification)

 1973 & 1974 guest lecturer
 Information Sciences Dept
 University of Cal
 Santa Cruz, Cal
    (Each year a two-week session on LISP and data stuctures for the
     graduate workshop)

 1975 lecturer (current)
 Mathematics Dept
 San Jose State University
 San Jose, Cal
   (Teaching a one-semester course on abstract programming, LISP,
    data structures, and translator construction; 
    uses my manuscript(see below))

Publications:
Various very old technical reports from Burroughs and General Motors

McCarthy, et.al. Thor - A Display Based Time Sharing System
 AFIPS Vol 30, 1967

Allen & Luckham, An Interactive Theorem-Proving Program
 Machine Intelligence Vol 5. 1970

Allen, The Anatomy of a Language (tentative title)
 book on language design, abstract programming, data structures, LISP, ...
 to be published by McGraw-Hill

Various SAIL memos: Documentation on LISP 1.6, A LISP editor (ALVINE)
 and user's manual for the theorem prover.

Organizations:
 ACM, SIGACT, SIGART, SIGOPS, SIGPLAN

Interests (in alphabetical order):
  Education: I am quite interested in the development better programs
  for  the education of  future Computer Scientists.   I particularly
  object to  the style  and content  of introductory  (undergraduate)
  courses.  My book  is  a  realization of  many  of  my ideas  about
  education and  some of my research interests involve development of
  a programming environment to reenforce these educational policies. 
  I have written (and had accepted for publication) a  letter  to the 
  ACM Forum attacking the current ACM68 course structure.

  Interactive systems: I am particularly interested in establishing a
  display   based  programming   laboratory  to   support  interative
  construction of correct or reliable programs. 

  Language design: One of the difficulties involved in getting  clean
  and correct programs written is the generally  poor state of curent
  programming languages. Most were developed with batch-processing in
  mind. Few  were developed  with any  consideration towards  on-line
  construction,  and even  fewer  considered the  problem of  proving
  correctness  of  the  programs.   Just  as  the  early  '60s  saw a
  structuring  of  language  design  to  conform   to  the  syntactic
  constraints of BNF, we  should consider the semantic constraints of
  correctness when we propose new languages. 

  Mathematical  semantics:   One  of   the  current   roadblocks   to
  correctness and reliability is a lack of knowledge about the "rules
  of   inference"  for  program  construction.   Several  schools  of
  semantics of programming language  exist. It will be through  these
  investigations  that we  will be  able to  put firm  foundations on
  programming constructs. 

I  am  currently  writing  a  proposal  to  begin  development  of  a
programming  laboratory  which  will implement  my  current  ideas on
program construction, correctness, and programming style.